Left Termination proof of /tmp/tmpUCofzo/dis

Left Termination of the query pattern dis_in_1(g) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

dis(or(B1, B2)) :- ','(con(B1), dis(B2)).
dis(B) :- con(B).
con(and(B1, B2)) :- ','(dis(B1), con(B2)).
con(B) :- bool(B).
bool(0).
bool(1).

Queries:

dis(g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
dis_in: (b)
con_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B1, B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B1, B2, dis_in_g(B1))
dis_in_g(B) → U3_g(B, con_in_g(B))
con_in_g(B) → U6_g(B, bool_in_g(B))
bool_in_g(0) → bool_out_g(0)
bool_in_g(1) → bool_out_g(1)
U6_g(B, bool_out_g(B)) → con_out_g(B)
U3_g(B, con_out_g(B)) → dis_out_g(B)
U4_g(B1, B2, dis_out_g(B1)) → U5_g(B1, B2, con_in_g(B2))
U5_g(B1, B2, con_out_g(B2)) → con_out_g(and(B1, B2))
U1_g(B1, B2, con_out_g(B1)) → U2_g(B1, B2, dis_in_g(B2))
U2_g(B1, B2, dis_out_g(B2)) → dis_out_g(or(B1, B2))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B1, B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B1, B2, dis_in_g(B1))
dis_in_g(B) → U3_g(B, con_in_g(B))
con_in_g(B) → U6_g(B, bool_in_g(B))
bool_in_g(0) → bool_out_g(0)
bool_in_g(1) → bool_out_g(1)
U6_g(B, bool_out_g(B)) → con_out_g(B)
U3_g(B, con_out_g(B)) → dis_out_g(B)
U4_g(B1, B2, dis_out_g(B1)) → U5_g(B1, B2, con_in_g(B2))
U5_g(B1, B2, con_out_g(B2)) → con_out_g(and(B1, B2))
U1_g(B1, B2, con_out_g(B1)) → U2_g(B1, B2, dis_in_g(B2))
U2_g(B1, B2, dis_out_g(B2)) → dis_out_g(or(B1, B2))

The argument filtering Pi contains the following mapping:
dis_in_g(x1) = dis_in_g(x1)
or(x1, x2) = or(x1, x2)
U1_g(x1, x2, x3) = U1_g(x2, x3)
con_in_g(x1) = con_in_g(x1)
and(x1, x2) = and(x1, x2)
U4_g(x1, x2, x3) = U4_g(x2, x3)
U3_g(x1, x2) = U3_g(x2)
U6_g(x1, x2) = U6_g(x2)
bool_in_g(x1) = bool_in_g(x1)
0 = 0
bool_out_g(x1) = bool_out_g
1 = 1
con_out_g(x1) = con_out_g
dis_out_g(x1) = dis_out_g
U5_g(x1, x2, x3) = U5_g(x3)
U2_g(x1, x2, x3) = U2_g(x3)

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DIS_IN_G(or(B1, B2)) → U1_G(B1, B2, con_in_g(B1))
DIS_IN_G(or(B1, B2)) → CON_IN_G(B1)
CON_IN_G(and(B1, B2)) → U4_G(B1, B2, dis_in_g(B1))
CON_IN_G(and(B1, B2)) → DIS_IN_G(B1)
DIS_IN_G(B) → U3_G(B, con_in_g(B))
DIS_IN_G(B) → CON_IN_G(B)
CON_IN_G(B) → U6_G(B, bool_in_g(B))
CON_IN_G(B) → BOOL_IN_G(B)
U4_G(B1, B2, dis_out_g(B1)) → U5_G(B1, B2, con_in_g(B2))
U4_G(B1, B2, dis_out_g(B1)) → CON_IN_G(B2)
U1_G(B1, B2, con_out_g(B1)) → U2_G(B1, B2, dis_in_g(B2))
U1_G(B1, B2, con_out_g(B1)) → DIS_IN_G(B2)

The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B1, B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B1, B2, dis_in_g(B1))
dis_in_g(B) → U3_g(B, con_in_g(B))
con_in_g(B) → U6_g(B, bool_in_g(B))
bool_in_g(0) → bool_out_g(0)
bool_in_g(1) → bool_out_g(1)
U6_g(B, bool_out_g(B)) → con_out_g(B)
U3_g(B, con_out_g(B)) → dis_out_g(B)
U4_g(B1, B2, dis_out_g(B1)) → U5_g(B1, B2, con_in_g(B2))
U5_g(B1, B2, con_out_g(B2)) → con_out_g(and(B1, B2))
U1_g(B1, B2, con_out_g(B1)) → U2_g(B1, B2, dis_in_g(B2))
U2_g(B1, B2, dis_out_g(B2)) → dis_out_g(or(B1, B2))

The argument filtering Pi contains the following mapping:
dis_in_g(x1) = dis_in_g(x1)
or(x1, x2) = or(x1, x2)
U1_g(x1, x2, x3) = U1_g(x2, x3)
con_in_g(x1) = con_in_g(x1)
and(x1, x2) = and(x1, x2)
U4_g(x1, x2, x3) = U4_g(x2, x3)
U3_g(x1, x2) = U3_g(x2)
U6_g(x1, x2) = U6_g(x2)
bool_in_g(x1) = bool_in_g(x1)
0 = 0
bool_out_g(x1) = bool_out_g
1 = 1
con_out_g(x1) = con_out_g
dis_out_g(x1) = dis_out_g
U5_g(x1, x2, x3) = U5_g(x3)
U2_g(x1, x2, x3) = U2_g(x3)
DIS_IN_G(x1) = DIS_IN_G(x1)
U2_G(x1, x2, x3) = U2_G(x3)
U4_G(x1, x2, x3) = U4_G(x2, x3)
U6_G(x1, x2) = U6_G(x2)
U5_G(x1, x2, x3) = U5_G(x3)
U1_G(x1, x2, x3) = U1_G(x2, x3)
U3_G(x1, x2) = U3_G(x2)
CON_IN_G(x1) = CON_IN_G(x1)
BOOL_IN_G(x1) = BOOL_IN_G(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

DIS_IN_G(or(B1, B2)) → U1_G(B1, B2, con_in_g(B1))
DIS_IN_G(or(B1, B2)) → CON_IN_G(B1)
CON_IN_G(and(B1, B2)) → U4_G(B1, B2, dis_in_g(B1))
CON_IN_G(and(B1, B2)) → DIS_IN_G(B1)
DIS_IN_G(B) → U3_G(B, con_in_g(B))
DIS_IN_G(B) → CON_IN_G(B)
CON_IN_G(B) → U6_G(B, bool_in_g(B))
CON_IN_G(B) → BOOL_IN_G(B)
U4_G(B1, B2, dis_out_g(B1)) → U5_G(B1, B2, con_in_g(B2))
U4_G(B1, B2, dis_out_g(B1)) → CON_IN_G(B2)
U1_G(B1, B2, con_out_g(B1)) → U2_G(B1, B2, dis_in_g(B2))
U1_G(B1, B2, con_out_g(B1)) → DIS_IN_G(B2)

The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B1, B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B1, B2, dis_in_g(B1))
dis_in_g(B) → U3_g(B, con_in_g(B))
con_in_g(B) → U6_g(B, bool_in_g(B))
bool_in_g(0) → bool_out_g(0)
bool_in_g(1) → bool_out_g(1)
U6_g(B, bool_out_g(B)) → con_out_g(B)
U3_g(B, con_out_g(B)) → dis_out_g(B)
U4_g(B1, B2, dis_out_g(B1)) → U5_g(B1, B2, con_in_g(B2))
U5_g(B1, B2, con_out_g(B2)) → con_out_g(and(B1, B2))
U1_g(B1, B2, con_out_g(B1)) → U2_g(B1, B2, dis_in_g(B2))
U2_g(B1, B2, dis_out_g(B2)) → dis_out_g(or(B1, B2))

The argument filtering Pi contains the following mapping:
dis_in_g(x1) = dis_in_g(x1)
or(x1, x2) = or(x1, x2)
U1_g(x1, x2, x3) = U1_g(x2, x3)
con_in_g(x1) = con_in_g(x1)
and(x1, x2) = and(x1, x2)
U4_g(x1, x2, x3) = U4_g(x2, x3)
U3_g(x1, x2) = U3_g(x2)
U6_g(x1, x2) = U6_g(x2)
bool_in_g(x1) = bool_in_g(x1)
0 = 0
bool_out_g(x1) = bool_out_g
1 = 1
con_out_g(x1) = con_out_g
dis_out_g(x1) = dis_out_g
U5_g(x1, x2, x3) = U5_g(x3)
U2_g(x1, x2, x3) = U2_g(x3)
DIS_IN_G(x1) = DIS_IN_G(x1)
U2_G(x1, x2, x3) = U2_G(x3)
U4_G(x1, x2, x3) = U4_G(x2, x3)
U6_G(x1, x2) = U6_G(x2)
U5_G(x1, x2, x3) = U5_G(x3)
U1_G(x1, x2, x3) = U1_G(x2, x3)
U3_G(x1, x2) = U3_G(x2)
CON_IN_G(x1) = CON_IN_G(x1)
BOOL_IN_G(x1) = BOOL_IN_G(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 5 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

DIS_IN_G(B) → CON_IN_G(B)
DIS_IN_G(or(B1, B2)) → U1_G(B1, B2, con_in_g(B1))
U1_G(B1, B2, con_out_g(B1)) → DIS_IN_G(B2)
DIS_IN_G(or(B1, B2)) → CON_IN_G(B1)
CON_IN_G(and(B1, B2)) → DIS_IN_G(B1)
U4_G(B1, B2, dis_out_g(B1)) → CON_IN_G(B2)
CON_IN_G(and(B1, B2)) → U4_G(B1, B2, dis_in_g(B1))

The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B1, B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B1, B2, dis_in_g(B1))
dis_in_g(B) → U3_g(B, con_in_g(B))
con_in_g(B) → U6_g(B, bool_in_g(B))
bool_in_g(0) → bool_out_g(0)
bool_in_g(1) → bool_out_g(1)
U6_g(B, bool_out_g(B)) → con_out_g(B)
U3_g(B, con_out_g(B)) → dis_out_g(B)
U4_g(B1, B2, dis_out_g(B1)) → U5_g(B1, B2, con_in_g(B2))
U5_g(B1, B2, con_out_g(B2)) → con_out_g(and(B1, B2))
U1_g(B1, B2, con_out_g(B1)) → U2_g(B1, B2, dis_in_g(B2))
U2_g(B1, B2, dis_out_g(B2)) → dis_out_g(or(B1, B2))

The argument filtering Pi contains the following mapping:
dis_in_g(x1) = dis_in_g(x1)
or(x1, x2) = or(x1, x2)
U1_g(x1, x2, x3) = U1_g(x2, x3)
con_in_g(x1) = con_in_g(x1)
and(x1, x2) = and(x1, x2)
U4_g(x1, x2, x3) = U4_g(x2, x3)
U3_g(x1, x2) = U3_g(x2)
U6_g(x1, x2) = U6_g(x2)
bool_in_g(x1) = bool_in_g(x1)
0 = 0
bool_out_g(x1) = bool_out_g
1 = 1
con_out_g(x1) = con_out_g
dis_out_g(x1) = dis_out_g
U5_g(x1, x2, x3) = U5_g(x3)
U2_g(x1, x2, x3) = U2_g(x3)
DIS_IN_G(x1) = DIS_IN_G(x1)
U4_G(x1, x2, x3) = U4_G(x2, x3)
U1_G(x1, x2, x3) = U1_G(x2, x3)
CON_IN_G(x1) = CON_IN_G(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

DIS_IN_G(B) → CON_IN_G(B)
DIS_IN_G(or(B1, B2)) → U1_G(B2, con_in_g(B1))
CON_IN_G(and(B1, B2)) → U4_G(B2, dis_in_g(B1))
DIS_IN_G(or(B1, B2)) → CON_IN_G(B1)
U1_G(B2, con_out_g) → DIS_IN_G(B2)
U4_G(B2, dis_out_g) → CON_IN_G(B2)
CON_IN_G(and(B1, B2)) → DIS_IN_G(B1)

The TRS R consists of the following rules:

dis_in_g(or(B1, B2)) → U1_g(B2, con_in_g(B1))
con_in_g(and(B1, B2)) → U4_g(B2, dis_in_g(B1))
dis_in_g(B) → U3_g(con_in_g(B))
con_in_g(B) → U6_g(bool_in_g(B))
bool_in_g(0) → bool_out_g
bool_in_g(1) → bool_out_g
U6_g(bool_out_g) → con_out_g
U3_g(con_out_g) → dis_out_g
U4_g(B2, dis_out_g) → U5_g(con_in_g(B2))
U5_g(con_out_g) → con_out_g
U1_g(B2, con_out_g) → U2_g(dis_in_g(B2))
U2_g(dis_out_g) → dis_out_g

The set Q consists of the following terms:

dis_in_g(x0)
con_in_g(x0)
bool_in_g(x0)
U6_g(x0)
U3_g(x0)
U4_g(x0, x1)
U5_g(x0)
U1_g(x0, x1)
U2_g(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

CON_IN_G(and(B1, B2)) → DIS_IN_G(B1)
The graph contains the following edges 1 > 1
CON_IN_G(and(B1, B2)) → U4_G(B2, dis_in_g(B1))
The graph contains the following edges 1 > 1
U1_G(B2, con_out_g) → DIS_IN_G(B2)
The graph contains the following edges 1 >= 1
DIS_IN_G(or(B1, B2)) → U1_G(B2, con_in_g(B1))
The graph contains the following edges 1 > 1
U4_G(B2, dis_out_g) → CON_IN_G(B2)
The graph contains the following edges 1 >= 1
DIS_IN_G(B) → CON_IN_G(B)
The graph contains the following edges 1 >= 1
DIS_IN_G(or(B1, B2)) → CON_IN_G(B1)
The graph contains the following edges 1 > 1